This invention relates to control-intensive systems, and more particularly to the development of finite state machine implementations of such systems through a methodology based upon formal verifications.
Digital circuits that have memory are commonly referred to as sequential circuits or finite state machines. Finite state machines can be divided into two categories. One is signal processing machines whose proper operations must be described in terms of a routine which calls itself recursively, and the other is non-recursive control-intensive machines. FIR filters, for example, belong to the first category. Communication protocol hardware belongs to the second category. Design of control-intensive finite state machines is a difficult task. Typically, the objective of such a design is to efficiently and quickly develop an implementation that is correct, robust with respect to changes in data structures and easy to support.
The value of a particular formal verification framework may be measured by the scope of generality of the requirements for which an implementation may be tested. For example, one can verify that at each state the protocol will not do anything untoward. This may be sufficient in some applications and not in others. In connection with communications protocols, for instance, such verification is not sufficient because the primary concern is that a message should be received at the destination, and such verification cannot guarantee that.
In order to ensure proper behavior of an implementation, extensive behavioral testing must be conducted. Normally that would imply extensive simulation, but it is now generally accepted that simulation is inadequate (the set of possible sequences of input signals that must be simulated for complete confidence is infinite). Formal verification techniques, on the other hand, can have the power to draw conclusions about the general behavior of a system under all situations through a finite test.
Since requirements address broad properties of a finite state machine, formal verification is most easily and most often applied to a high-level model or abstraction of the implementation. Such verification is not enough. For verification of a high-level model to have real meaning for an implementation, there must exist a formal association or transformation from the high-level model to the implementation.
Even in the absence of a formal transformation from an abstract model to its actual implementation, formal analysis of the model is useful. In connection with finite state machines that embody a protocol, for example, formal analysis discloses faults in the very concept of the protocol itself. However, it is deceptive to refer to an implementation as "verified" in the absence of such faults if there is no formal, testable, relationship between the verified model and its actual implementation.
A simple way to define a formal relationship between a high-level model or standard and an implementation is to associate a state in the model or standard with a set of states of the implementation. Such an association, for example, may require that the Receiver-Ready state of the high-level model of a communications protocol correspond to the set of implementation states for which a certain state machine component of the protocol implementation is in its Receiver-Ready state. The set of implementation states for which this state machine component is in the Receiver-Ready state may be very large since the state is determined by all the possible respective values of pointers, buffers, counters and so on in the circuit which may occur together with the state machine component having state Receiver-Ready. If one were to suppose that according to the high-level model or standard, the correct transition from Receiver-Ready is to the state Transmit, still it may be that for certain implementation states (i.e., for certain values of pointers, buffers and so on) the implementation tracks the model or standard, while for others it does not. To certify truly that a high-level model or standard abstracts an implementation, it would be necessary to demonstrate this abstraction not only for a single implementation state and transition corresponding to each respective high-level state and transition, but rather for every low-level state and transition. Indeed, it is well-known that the greatest weaknesses of an implementation arise at the "boundaries" of operation (buffer empty, buffer full, etc.) and that these "boundaries" can be very complex.
As intimated above, one could use the brute force technique of simulating all possible states of the model (i.e., all possible combinations of pointers, buffers, etc.), but this is rarely practical. While a high-level model or standard may have as few as 50 to 500 states, an implementation typically has such a large number of states that the number can be appreciated only by analogy. For example, given all the possible combined values of its pointers, buffers and state machine controllers of an "average" protocol implementation, it turns out that the state space of a circuit contains approximately 10.sup.10.spsp.4 reachable states. Supposing that a brute force verification algorithm were perfectly parallelizable among every human being on earth, and each person, in order to accomplish his or her piece of the work, were given a super computer. With 10.sup.10.sbsb.4 states, the verification job could not be completed before the sun turned to stone.
Since it is rarely feasible to address directly all possible transitions of an implementation (i.e., to address all possible values of pointers, buffers, etc.), there must be an alternative by which to conclude that an implementation is faithful to its high-level abstraction.
Lastly, having formal verification together with a comprehensive and a proven method for transforming high level description to low level specifications is still insufficient in light of the tremendous complexity that finite state machines may represent. To reduce this complexity, artisans have attempted to replace complex problems with simpler presentations. K. G. Larsen et al. in Lecture Notes in Computer Science, Springer-Verlag, 14th International Colloquium Karlsruhe, Federal Republic of Germany, July 13-17, 1987 Proceedings, presented a compositional proof, by decomposing the system and demonstrating properties of the subsystems that are strong enough to hold true for the complete system. However, they have not provided a methodology for proving that their substitutions (of complex problems with simple problem equivalent) are valid.
In short, what is needed to the development of control-intensive FSM's is an automated software-aided design approach that incorporates formal verification, formal behavior-preserving transformation from a high-level design to a refined implementation, and the means to manage the ensuing complexity brought on by the refined implementations.